{-| 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 Data.Data (Data(..))
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      = Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
0
  prettyPrec  = (a -> Doc) -> Int -> a -> Doc
forall a b. a -> b -> a
const a -> Doc
forall a. Pretty a => a -> Doc
pretty
  prettyList  = Doc -> Doc
brackets (Doc -> Doc) -> ([a] -> Doc) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList_

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

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

-- * Pretty instances

instance Pretty Bool    where pretty :: Bool -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Bool -> String) -> Bool -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
forall a. Show a => a -> String
show
instance Pretty Int     where pretty :: Int -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Int -> String) -> Int -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show
instance Pretty Int32   where pretty :: Int32 -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Int32 -> String) -> Int32 -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int32 -> String
forall a. Show a => a -> String
show
instance Pretty Integer where pretty :: Integer -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Integer -> String) -> Integer -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show
instance Pretty Word64  where pretty :: Word64 -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Word64 -> String) -> Word64 -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> String
forall a. Show a => a -> String
show
instance Pretty Double  where pretty :: Double -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Double -> String) -> Double -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> String
toStringWithoutDotZero
instance Pretty Text    where pretty :: Text -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Text -> String) -> Text -> Doc
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 = Doc -> Doc
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) = Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p a
x

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

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

instance Pretty IntSet where
  pretty :: IntSet -> Doc
pretty = [Int] -> Doc
forall a. Pretty a => [a] -> Doc
prettySet ([Int] -> Doc) -> (IntSet -> [Int]) -> IntSet -> Doc
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 = [a] -> Doc
forall a. Pretty a => [a] -> Doc
prettySet ([a] -> Doc) -> (Set a -> [a]) -> Set a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Set.toList

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

instance (Pretty k, Pretty v) => Pretty (Map k v) where
  pretty :: Map k v -> Doc
pretty = [(k, v)] -> Doc
forall k v. (Pretty k, Pretty v) => [(k, v)] -> Doc
prettyMap ([(k, v)] -> Doc) -> (Map k v -> [(k, v)]) -> Map k v -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map k v -> [(k, v)]
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 :: t Doc -> Doc
sep  = [Doc] -> Doc
P.sep  ([Doc] -> Doc) -> (t Doc -> [Doc]) -> t Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t Doc -> [Doc]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList
fsep :: t Doc -> Doc
fsep = [Doc] -> Doc
P.fsep ([Doc] -> Doc) -> (t Doc -> [Doc]) -> t Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t Doc -> [Doc]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList
hsep :: t Doc -> Doc
hsep = [Doc] -> Doc
P.hsep ([Doc] -> Doc) -> (t Doc -> [Doc]) -> t Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t Doc -> [Doc]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList
hcat :: t Doc -> Doc
hcat = [Doc] -> Doc
P.hcat ([Doc] -> Doc) -> (t Doc -> [Doc]) -> t Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t Doc -> [Doc]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList
vcat :: t Doc -> Doc
vcat = [Doc] -> Doc
P.vcat ([Doc] -> Doc) -> (t Doc -> [Doc]) -> t Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t Doc -> [Doc]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList

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

-- * 'Doc' utilities

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

fwords :: String -> Doc
fwords :: String -> Doc
fwords = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> (String -> [Doc]) -> String -> Doc
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
  | Doc -> Bool
forall a. Null a => a -> Bool
null Doc
d2   = Doc
d1
  | Doc -> Bool
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_ :: [a] -> Doc
prettyList_ = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> ([a] -> [Doc]) -> [a] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty

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

-- | Pretty print an association list.
prettyMap :: (Pretty k, Pretty v) => [(k,v)] -> Doc
prettyMap :: [(k, v)] -> Doc
prettyMap = Doc -> Doc
braces (Doc -> Doc) -> ([(k, v)] -> Doc) -> [(k, v)] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> ([(k, v)] -> [Doc]) -> [(k, v)] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> ([(k, v)] -> [Doc]) -> [(k, v)] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, v) -> Doc) -> [(k, v)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (k, v) -> Doc
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 :: (k, v) -> Doc
prettyAssign (k
k, v
v) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Int -> k -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
1 k
k Doc -> Doc -> Doc
<+> Doc
"->", Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ v -> Doc
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 = Doc -> Doc
forall a. a -> a
id

-- | Only wrap in parens if not 'empty'
parensNonEmpty :: Doc -> Doc
parensNonEmpty :: Doc -> Doc
parensNonEmpty Doc
d = if Doc -> Bool
forall a. Null a => a -> Bool
null Doc
d then Doc
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 =
  [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((String, Doc) -> Doc) -> [(String, Doc)] -> [Doc]
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Doc
d) ([(String, Doc)] -> [Doc]) -> [(String, Doc)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ [(String, Doc)]
rows
  where maxLen :: Int
maxLen = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
max) (((String, Doc) -> Int) -> [(String, Doc)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int)
-> ((String, Doc) -> String) -> (String, Doc) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Doc) -> String
forall a b. (a, b) -> a
fst) [(String, Doc)]
rows)

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

-- cheating because you shouldn't be digging this far anyway
instance Data Doc where
  gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Doc
gunfold forall b r. Data b => c (b -> r) -> c r
_ forall r. r -> c r
_ Constr
_ = c Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
  toConstr :: Doc -> Constr
toConstr      = Doc -> Constr
forall a. HasCallStack => a
__IMPOSSIBLE__
  dataTypeOf :: Doc -> DataType
dataTypeOf    = Doc -> DataType
forall a. HasCallStack => a
__IMPOSSIBLE__

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 :: a -> Doc
pshow = String -> Doc
text (String -> Doc) -> (a -> String) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. Show a => a -> String
show

singPlural :: Sized a => a -> c -> c -> c
singPlural :: a -> c -> c -> c
singPlural a
xs c
singular c
plural = if a -> Int
forall a. Sized a => a -> Int
size a
xs Int -> Int -> Bool
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) -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc
kw Doc -> Doc -> Doc
<+> Doc
doc) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Doc -> Doc) -> [Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc
"|" Doc -> Doc -> Doc
<+>) [Doc]
docs