{-| Pretty printing functions.
-}
module Agda.Utils.Pretty
    ( module Agda.Utils.Pretty
    , module Text.PrettyPrint
    -- This re-export can be removed once <GHC-8.4 is dropped.
    , module Data.Semigroup
    ) where

import Prelude hiding (null)

import qualified Data.Foldable as Fold
import Data.Int (Int32)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as T
import Data.Word (Word64)

import qualified Text.PrettyPrint as P
import Text.PrettyPrint hiding (TextDetails(Str), empty, (<>), sep, fsep, hsep, hcat, vcat, punctuate)
import Data.Semigroup ((<>))

import Agda.Utils.Float
import Agda.Utils.List1 (List1)
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Utils.Size

import Agda.Utils.Impossible

-- * Pretty class

-- | While 'Show' is for rendering data in Haskell syntax,
--   'Pretty' is for displaying data to the world, i.e., the
--   user and the environment.
--
--   Atomic data has no inner document structure, so just
--   implement 'pretty' as @pretty a = text $ ... a ...@.

class Pretty a where
  pretty      :: a -> Doc
  prettyPrec  :: Int -> a -> Doc
  prettyList  :: [a] -> Doc

  pretty      = forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
0
  prettyPrec  = forall a b. a -> b -> a
const forall a. Pretty a => a -> Doc
pretty
  prettyList  = Doc -> Doc
brackets forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => [a] -> Doc
prettyList_

-- | Use instead of 'show' when printing to world.

prettyShow :: Pretty a => a -> String
prettyShow :: forall a. Pretty a => a -> String
prettyShow = Doc -> String
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty

-- * Pretty instances

instance Pretty Bool    where pretty :: Bool -> Doc
pretty = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show
instance Pretty Int     where pretty :: Int -> Doc
pretty = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show
instance Pretty Int32   where pretty :: Int32 -> Doc
pretty = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show
instance Pretty Integer where pretty :: Integer -> Doc
pretty = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show
instance Pretty Word64  where pretty :: Word64 -> Doc
pretty = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show
instance Pretty Double  where pretty :: Double -> Doc
pretty = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> String
toStringWithoutDotZero
instance Pretty Text    where pretty :: Text -> Doc
pretty = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack

instance Pretty Char where
  pretty :: Char -> Doc
pretty Char
c = String -> Doc
text [Char
c]
  prettyList :: String -> Doc
prettyList = String -> Doc
text

instance Pretty Doc where
  pretty :: Doc -> Doc
pretty = forall a. a -> a
id

instance Pretty () where
  pretty :: () -> Doc
pretty ()
_ = Doc
P.empty

instance Pretty a => Pretty (Maybe a) where
  prettyPrec :: Int -> Maybe a -> Doc
prettyPrec Int
p Maybe a
Nothing  = Doc
"(nothing)"
  prettyPrec Int
p (Just a
x) = forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p a
x

instance Pretty a => Pretty [a] where
  pretty :: [a] -> Doc
pretty = forall a. Pretty a => [a] -> Doc
prettyList

instance Pretty a => Pretty (List1 a) where
  pretty :: List1 a -> Doc
pretty = forall a. Pretty a => [a] -> Doc
prettyList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. IsList l => l -> [Item l]
List1.toList

instance Pretty IntSet where
  pretty :: IntSet -> Doc
pretty = forall a. Pretty a => [a] -> Doc
prettySet forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IntSet.toList

instance Pretty a => Pretty (Set a) where
  pretty :: Set a -> Doc
pretty = forall a. Pretty a => [a] -> Doc
prettySet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList

instance Pretty a => Pretty (IntMap a) where
  pretty :: IntMap a -> Doc
pretty = forall k v. (Pretty k, Pretty v) => [(k, v)] -> Doc
prettyMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IntMap a -> [(Int, a)]
IntMap.toList

instance (Pretty k, Pretty v) => Pretty (Map k v) where
  pretty :: Map k v -> Doc
pretty = forall k v. (Pretty k, Pretty v) => [(k, v)] -> Doc
prettyMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
Map.toList

-- * Generalizing the original type from list to Foldable

sep, fsep, hsep, hcat, vcat :: Foldable t => t Doc -> Doc
sep :: forall (t :: * -> *). Foldable t => t Doc -> Doc
sep  = [Doc] -> Doc
P.sep  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList
fsep :: forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep = [Doc] -> Doc
P.fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList
hsep :: forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep = [Doc] -> Doc
P.hsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList
hcat :: forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat = [Doc] -> Doc
P.hcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList
vcat :: forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat = [Doc] -> Doc
P.vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList

punctuate :: Foldable t => Doc -> t Doc -> [Doc]
punctuate :: forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
d = Doc -> [Doc] -> [Doc]
P.punctuate Doc
d forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList

-- * 'Doc' utilities

pwords :: String -> [Doc]
pwords :: String -> [Doc]
pwords = forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words

fwords :: String -> Doc
fwords :: String -> Doc
fwords = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Doc]
pwords

-- | Separate, but only if both separees are not null.

hsepWith :: Doc -> Doc -> Doc -> Doc
hsepWith :: Doc -> Doc -> Doc -> Doc
hsepWith Doc
sep Doc
d1 Doc
d2
  | forall a. Null a => a -> Bool
null Doc
d2   = Doc
d1
  | forall a. Null a => a -> Bool
null Doc
d1   = Doc
d2
  | Bool
otherwise = Doc
d1 Doc -> Doc -> Doc
<+> Doc
sep Doc -> Doc -> Doc
<+> Doc
d2

-- | Comma separated list, without the brackets.
prettyList_ :: Pretty a => [a] -> Doc
prettyList_ :: forall a. Pretty a => [a] -> Doc
prettyList_ = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty

-- | Pretty print a set.
prettySet :: Pretty a => [a] -> Doc
prettySet :: forall a. Pretty a => [a] -> Doc
prettySet = Doc -> Doc
braces forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => [a] -> Doc
prettyList_

-- | Pretty print an association list.
prettyMap :: (Pretty k, Pretty v) => [(k,v)] -> Doc
prettyMap :: forall k v. (Pretty k, Pretty v) => [(k, v)] -> Doc
prettyMap = Doc -> Doc
braces forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall k v. (Pretty k, Pretty v) => (k, v) -> Doc
prettyAssign

-- | Pretty print a single association.
prettyAssign :: (Pretty k, Pretty v) => (k,v) -> Doc
prettyAssign :: forall k v. (Pretty k, Pretty v) => (k, v) -> Doc
prettyAssign (k
k, v
v) = forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
1 k
k Doc -> Doc -> Doc
<+> Doc
"->", Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty v
v ]

-- ASR (2016-12-13): In pretty >= 1.1.2.0 the below function 'mparens'
-- is called 'maybeParens'. I didn't use that name due to the issue
-- https://github.com/haskell/pretty/issues/40.

-- | Apply 'parens' to 'Doc' if boolean is true.
mparens :: Bool -> Doc -> Doc
mparens :: Bool -> Doc -> Doc
mparens Bool
True  = Doc -> Doc
parens
mparens Bool
False = forall a. a -> a
id

-- | Only wrap in parens if not 'empty'
parensNonEmpty :: Doc -> Doc
parensNonEmpty :: Doc -> Doc
parensNonEmpty Doc
d = if forall a. Null a => a -> Bool
null Doc
d then forall a. Null a => a
empty else Doc -> Doc
parens Doc
d

-- | @align max rows@ lays out the elements of @rows@ in two columns,
-- with the second components aligned. The alignment column of the
-- second components is at most @max@ characters to the right of the
-- left-most column.
--
-- Precondition: @max > 0@.

align :: Int -> [(String, Doc)] -> Doc
align :: Int -> [(String, Doc)] -> Doc
align Int
max [(String, Doc)]
rows =
  forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(String
s, Doc
d) -> String -> Doc
text String
s Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest (Int
maxLen forall a. Num a => a -> a -> a
+ Int
1) Doc
d) forall a b. (a -> b) -> a -> b
$ [(String, Doc)]
rows
  where maxLen :: Int
maxLen = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ Int
0 forall a. a -> [a] -> [a]
: forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> a -> Bool
< Int
max) (forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(String, Doc)]
rows)

-- | Handles strings with newlines properly (preserving indentation)
multiLineText :: String -> Doc
multiLineText :: String -> Doc
multiLineText = forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines

infixl 6 <?>
-- | @a <?> b = hang a 2 b@
(<?>) :: Doc -> Doc -> Doc
Doc
a <?> :: Doc -> Doc -> Doc
<?> Doc
b = Doc -> Int -> Doc -> Doc
hang Doc
a Int
2 Doc
b

-- | @pshow = text . show@
pshow :: Show a => a -> Doc
pshow :: forall a. Show a => a -> Doc
pshow = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

singPlural :: Sized a => a -> c -> c -> c
singPlural :: forall a c. Sized a => a -> c -> c -> c
singPlural a
xs c
singular c
plural = if forall a. Sized a => a -> Int
size a
xs forall a. Eq a => a -> a -> Bool
== Int
1 then c
singular else c
plural

-- | Used for with-like 'telescopes'

prefixedThings :: Doc -> [Doc] -> Doc
prefixedThings :: Doc -> [Doc] -> Doc
prefixedThings Doc
kw = \case
  []           -> Doc
P.empty
  (Doc
doc : [Doc]
docs) -> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$ (Doc
kw Doc -> Doc -> Doc
<+> Doc
doc) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (Doc
"|" Doc -> Doc -> Doc
<+>) [Doc]
docs