1 2{-| Pretty printing functions. 3-} 4module Agda.Utils.Pretty 5 ( module Agda.Utils.Pretty 6 , module Text.PrettyPrint 7 -- This re-export can be removed once <GHC-8.4 is dropped. 8 , module Data.Semigroup 9 ) where 10 11import Prelude hiding (null) 12 13import Data.Data (Data(..)) 14import qualified Data.Foldable as Fold 15import Data.Int (Int32) 16import Data.IntSet (IntSet) 17import qualified Data.IntSet as IntSet 18import Data.IntMap (IntMap) 19import qualified Data.IntMap as IntMap 20import Data.Map (Map) 21import qualified Data.Map as Map 22import Data.Set (Set) 23import qualified Data.Set as Set 24import Data.Text (Text) 25import qualified Data.Text as T 26import Data.Word (Word64) 27 28import qualified Text.PrettyPrint as P 29import Text.PrettyPrint hiding (TextDetails(Str), empty, (<>), sep, fsep, hsep, hcat, vcat, punctuate) 30import Data.Semigroup ((<>)) 31 32import Agda.Utils.Float 33import Agda.Utils.List1 (List1) 34import qualified Agda.Utils.List1 as List1 35import Agda.Utils.Null 36import Agda.Utils.Size 37 38import Agda.Utils.Impossible 39 40-- * Pretty class 41 42-- | While 'Show' is for rendering data in Haskell syntax, 43-- 'Pretty' is for displaying data to the world, i.e., the 44-- user and the environment. 45-- 46-- Atomic data has no inner document structure, so just 47-- implement 'pretty' as @pretty a = text $ ... a ...@. 48 49class Pretty a where 50 pretty :: a -> Doc 51 prettyPrec :: Int -> a -> Doc 52 prettyList :: [a] -> Doc 53 54 pretty = prettyPrec 0 55 prettyPrec = const pretty 56 prettyList = brackets . prettyList_ 57 58-- | Use instead of 'show' when printing to world. 59 60prettyShow :: Pretty a => a -> String 61prettyShow = render . pretty 62 63-- * Pretty instances 64 65instance Pretty Bool where pretty = text . show 66instance Pretty Int where pretty = text . show 67instance Pretty Int32 where pretty = text . show 68instance Pretty Integer where pretty = text . show 69instance Pretty Word64 where pretty = text . show 70instance Pretty Double where pretty = text . toStringWithoutDotZero 71instance Pretty Text where pretty = text . T.unpack 72 73instance Pretty Char where 74 pretty c = text [c] 75 prettyList = text 76 77instance Pretty Doc where 78 pretty = id 79 80instance Pretty () where 81 pretty _ = P.empty 82 83instance Pretty a => Pretty (Maybe a) where 84 prettyPrec p Nothing = "(nothing)" 85 prettyPrec p (Just x) = prettyPrec p x 86 87instance Pretty a => Pretty [a] where 88 pretty = prettyList 89 90instance Pretty a => Pretty (List1 a) where 91 pretty = prettyList . List1.toList 92 93instance Pretty IntSet where 94 pretty = prettySet . IntSet.toList 95 96instance Pretty a => Pretty (Set a) where 97 pretty = prettySet . Set.toList 98 99instance Pretty a => Pretty (IntMap a) where 100 pretty = prettyMap . IntMap.toList 101 102instance (Pretty k, Pretty v) => Pretty (Map k v) where 103 pretty = prettyMap . Map.toList 104 105-- * Generalizing the original type from list to Foldable 106 107sep, fsep, hsep, hcat, vcat :: Foldable t => t Doc -> Doc 108sep = P.sep . Fold.toList 109fsep = P.fsep . Fold.toList 110hsep = P.hsep . Fold.toList 111hcat = P.hcat . Fold.toList 112vcat = P.vcat . Fold.toList 113 114punctuate :: Foldable t => Doc -> t Doc -> [Doc] 115punctuate d = P.punctuate d . Fold.toList 116 117-- * 'Doc' utilities 118 119pwords :: String -> [Doc] 120pwords = map text . words 121 122fwords :: String -> Doc 123fwords = fsep . pwords 124 125-- | Separate, but only if both separees are not null. 126 127hsepWith :: Doc -> Doc -> Doc -> Doc 128hsepWith sep d1 d2 129 | null d2 = d1 130 | null d1 = d2 131 | otherwise = d1 <+> sep <+> d2 132 133-- | Comma separated list, without the brackets. 134prettyList_ :: Pretty a => [a] -> Doc 135prettyList_ = fsep . punctuate comma . map pretty 136 137-- | Pretty print a set. 138prettySet :: Pretty a => [a] -> Doc 139prettySet = braces . prettyList_ 140 141-- | Pretty print an association list. 142prettyMap :: (Pretty k, Pretty v) => [(k,v)] -> Doc 143prettyMap = braces . fsep . punctuate comma . map prettyAssign 144 145-- | Pretty print a single association. 146prettyAssign :: (Pretty k, Pretty v) => (k,v) -> Doc 147prettyAssign (k, v) = sep [ prettyPrec 1 k <+> "->", nest 2 $ pretty v ] 148 149-- ASR (2016-12-13): In pretty >= 1.1.2.0 the below function 'mparens' 150-- is called 'maybeParens'. I didn't use that name due to the issue 151-- https://github.com/haskell/pretty/issues/40. 152 153-- | Apply 'parens' to 'Doc' if boolean is true. 154mparens :: Bool -> Doc -> Doc 155mparens True = parens 156mparens False = id 157 158-- | Only wrap in parens if not 'empty' 159parensNonEmpty :: Doc -> Doc 160parensNonEmpty d = if null d then empty else parens d 161 162-- | @align max rows@ lays out the elements of @rows@ in two columns, 163-- with the second components aligned. The alignment column of the 164-- second components is at most @max@ characters to the right of the 165-- left-most column. 166-- 167-- Precondition: @max > 0@. 168 169align :: Int -> [(String, Doc)] -> Doc 170align max rows = 171 vcat $ map (\(s, d) -> text s $$ nest (maxLen + 1) d) $ rows 172 where maxLen = maximum $ 0 : filter (< max) (map (length . fst) rows) 173 174-- | Handles strings with newlines properly (preserving indentation) 175multiLineText :: String -> Doc 176multiLineText = vcat . map text . lines 177 178-- cheating because you shouldn't be digging this far anyway 179instance Data Doc where 180 gunfold _ _ _ = __IMPOSSIBLE__ 181 toConstr = __IMPOSSIBLE__ 182 dataTypeOf = __IMPOSSIBLE__ 183 184infixl 6 <?> 185-- | @a <?> b = hang a 2 b@ 186(<?>) :: Doc -> Doc -> Doc 187a <?> b = hang a 2 b 188 189-- | @pshow = text . show@ 190pshow :: Show a => a -> Doc 191pshow = text . show 192 193singPlural :: Sized a => a -> c -> c -> c 194singPlural xs singular plural = if size xs == 1 then singular else plural 195 196-- | Used for with-like 'telescopes' 197 198prefixedThings :: Doc -> [Doc] -> Doc 199prefixedThings kw = \case 200 [] -> P.empty 201 (doc : docs) -> fsep $ (kw <+> doc) : map ("|" <+>) docs 202