    {-| 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 :: forall a. Pretty a => 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 :: forall (t :: * -> *). Foldable t => 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 :: forall (t :: * -> *). Foldable t => 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 :: forall (t :: * -> *). Foldable t => 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 :: forall (t :: * -> *). Foldable t => 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 :: forall (t :: * -> *). Foldable t => 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 :: forall (t :: * -> *). Foldable t => 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_ :: forall a. Pretty a => [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 :: forall a. Pretty a => [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 :: forall k v. (Pretty k, Pretty v) => [(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 :: forall k v. (Pretty k, Pretty v) => (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 (c :: * -> *).
    (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 :: forall a. Show a => 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 :: forall a c. Sized a => 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