    {-# LANGUAGE CPP #-}

    {-| Pretty printing functions.
    -}
    module Agda.Utils.Pretty
        ( module Agda.Utils.Pretty
        , module Text.PrettyPrint
        ) where

    import Data.Int ( Int32 )
    import Data.Data (Data(..))
    import qualified Data.Map as Map

    #if __GLASGOW_HASKELL__ < 800
    import qualified Data.Semigroup as S
    #endif

    import qualified Text.PrettyPrint as P
    import Text.PrettyPrint hiding (TextDetails(Str), empty)

    import Agda.Utils.NonemptyList

    #include "undefined.h"
    import Agda.Utils.Impossible

    #if __GLASGOW_HASKELL__ < 800
    -- ASR (2019-03-27). I used @(<>)@ from the monoid instance because I
    -- cannot hide this instance.
    instance S.Semigroup Doc where
      (<>) = (<>)
    #endif

    -- * 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      = prettyPrec 0
      prettyPrec  = const pretty
      prettyList  = brackets . prettyList_

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

    prettyShow :: Pretty a => a -> String
    prettyShow = render . pretty

    -- * Pretty instances

    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 (NonemptyList a) where
      pretty = prettyList . toList

    -- * 'Doc' utilities

    pwords :: String -> [Doc]
    pwords = map text . words

    fwords :: String -> Doc
    fwords = fsep . pwords

    -- | Comma separated list, without the brackets.
    prettyList_ :: Pretty a => [a] -> Doc
    prettyList_ = fsep . punctuate comma . map 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 True  = parens
    mparens False = 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 max rows =
      vcat $ map (\(s, d) -> text s $$ nest (maxLen + 1) d) $ rows
      where maxLen = maximum $ 0 : filter (< max) (map (length . fst) rows)

    -- | Handles strings with newlines properly (preserving indentation)
    multiLineText :: String -> Doc
    multiLineText = vcat . map text . lines

    -- cheating because you shouldn't be digging this far anyway
    instance Data Doc where
      gunfold _ _ _ = __IMPOSSIBLE__
      toConstr      = __IMPOSSIBLE__
      dataTypeOf    = __IMPOSSIBLE__

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

    -- | @pshow = text . pretty@
    pshow :: Show a => a -> Doc
    pshow = text . show