{-| 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 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

-- * 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 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) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Just" Doc -> Doc -> Doc
<+> Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 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 (NonEmpty a) where
  pretty :: NonEmpty a -> Doc
pretty = [a] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList ([a] -> Doc) -> (NonEmpty a -> [a]) -> NonEmpty a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NonEmpty.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
fsep ([Doc] -> Doc) -> (String -> [Doc]) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Doc]
pwords

-- | Comma separated list, without the brackets.
prettyList_ :: Pretty a => [a] -> Doc
prettyList_ :: [a] -> Doc
prettyList_ = [Doc] -> Doc
fsep ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [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

-- 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

-- | @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
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
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 . pretty@
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
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