module Agda.Utils.Pretty
( module Agda.Utils.Pretty
, module Text.PrettyPrint
, module Data.Semigroup
) where
import Data.Int ( Int32 )
import Data.Data (Data(..))
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import qualified Text.PrettyPrint as P
import Text.PrettyPrint hiding (TextDetails(Str), empty, (<>))
import Data.Semigroup ((<>))
import Agda.Utils.Size
import Agda.Utils.Impossible
class Pretty a where
pretty :: a -> Doc
prettyPrec :: Int -> a -> Doc
prettyList :: [a] -> Doc
pretty = prettyPrec 0
prettyPrec = const pretty
prettyList = brackets . prettyList_
prettyShow :: Pretty a => a -> String
prettyShow = render . pretty
instance Pretty Bool where pretty = text . show
instance Pretty Int where pretty = text . show
instance Pretty Int32 where pretty = text . show
instance Pretty Integer where pretty = text . show
instance Pretty Char where
pretty c = text [c]
prettyList = text
instance Pretty Doc where
pretty = id
instance Pretty () where
pretty _ = P.empty
instance Pretty a => Pretty (Maybe a) where
prettyPrec p Nothing = "Nothing"
prettyPrec p (Just x) = mparens (p > 0) $ "Just" <+> prettyPrec 10 x
instance Pretty a => Pretty [a] where
pretty = prettyList
instance Pretty a => Pretty (NonEmpty a) where
pretty = prettyList . NonEmpty.toList
pwords :: String -> [Doc]
pwords = map text . words
fwords :: String -> Doc
fwords = fsep . pwords
prettyList_ :: Pretty a => [a] -> Doc
prettyList_ = fsep . punctuate comma . map pretty
mparens :: Bool -> Doc -> Doc
mparens True = parens
mparens False = id
align :: Int -> [(String, Doc)] -> Doc
align max rows =
vcat $ map (\(s, d) -> text s $$ nest (maxLen + 1) d) $ rows
where maxLen = maximum $ 0 : filter (< max) (map (length . fst) rows)
multiLineText :: String -> Doc
multiLineText = vcat . map text . lines
instance Data Doc where
gunfold _ _ _ = __IMPOSSIBLE__
toConstr = __IMPOSSIBLE__
dataTypeOf = __IMPOSSIBLE__
infixl 6 <?>
(<?>) :: Doc -> Doc -> Doc
a <?> b = hang a 2 b
pshow :: Show a => a -> Doc
pshow = text . show
singPlural :: Sized a => a -> c -> c -> c
singPlural xs singular plural = if size xs == 1 then singular else plural
prefixedThings :: Doc -> [Doc] -> Doc
prefixedThings kw = \case
[] -> P.empty
(doc : docs) -> fsep $ (kw <+> doc) : map ("|" <+>) docs