content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  {-| Pretty printing functions.
  -}
  module Agda.Syntax.Common.Pretty
      ( module Agda.Syntax.Common.Pretty
      , module Text.PrettyPrint.Annotated
      ) where
  
  import Prelude hiding (null)
  
  import Control.DeepSeq
  
  import qualified Data.List as List
  import qualified Data.Foldable as Fold
  import qualified Data.IntSet as IntSet
  import qualified Data.IntMap as IntMap
  import qualified Data.Text as T
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import Data.IntSet (IntSet)
  import Data.IntMap (IntMap)
  import Data.Word (Word64, Word32)
  import Data.Text (Text)
  import Data.Text qualified as Text
  import Data.Int (Int32)
  import Data.Map (Map)
  import Data.Set (Set)
  
  import qualified Text.PrettyPrint.Annotated as P
  import Text.PrettyPrint.Annotated hiding
    ( Doc, TextDetails(Str), empty, (<>), sep, fsep, hsep, hcat, vcat, punctuate
  
    , parens, brackets, braces, quotes, doubleQuotes
  
    , semi, comma, colon, space, equals, lparen, rparen, lbrack, rbrack
    , lbrace, rbrace
    , annotate
    )
  
  import Agda.Syntax.Common.Aspect
  import Agda.Syntax.Position
  
  import Agda.Utils.DocTree qualified as DocTree
  import Agda.Utils.FileName
  import Agda.Utils.Float
  import Agda.Utils.List1 (List1)
  import qualified Agda.Utils.List1 as List1
  import qualified Agda.Utils.Maybe.Strict as Strict
  import Agda.Utils.Null
  import Agda.Utils.Size
  
  type DocTree = DocTree.DocTree Aspects
  
  ---------------------------------------------------------------------------
  -- * Pretty class
  
  -- | The type of documents. We use documents annotated by 'Aspects' to
  -- record syntactic highlighting information that is generated during
  -- pretty-printing.
  type Doc = P.Doc Aspects
  
  -- | 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_
  
    {-# MINIMAL pretty | prettyPrec #-}
  
  -- | 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 Word32  where pretty = text . show
  instance Pretty Word64  where pretty = text . show
  instance Pretty Double  where pretty = text . toStringWithoutDotZero
  instance Pretty Text    where pretty = text . T.unpack
  
  instance Pretty Char where
    pretty c = text [c]
    prettyList = text
  
  
  -- The equational constraint forces GHC to pick this instance and unify
  -- the type variable, instead of deferring selection to when the type of
  -- annotations is solved.
  instance a ~ Aspects => Pretty (P.Doc a) where
    pretty = id
  
  instance a ~ Aspects => Pretty (DocTree.DocTree a) where
    pretty = DocTree.prettyDocTree
  
  instance Pretty () where
    pretty _ = P.empty
  
  instance (Pretty a, Pretty b) => Pretty (a, b) where
      pretty (a, b) = parens $ (pretty a <> comma) <+> pretty b
  
  instance Pretty a => Pretty (Maybe a) where
    prettyPrec p Nothing  = P.empty
    prettyPrec p (Just x) = prettyPrec p x
  
  instance Pretty a => Pretty [a] where
    pretty = prettyList
  
  instance Pretty a => Pretty (List1 a) where
    pretty = prettyList . List1.toList
  
  instance Pretty IntSet where
    pretty = prettySet . IntSet.toList
  
  instance Pretty a => Pretty (Set a) where
    pretty = prettySet . Set.toList
  
  instance Pretty a => Pretty (IntMap a) where
    pretty = prettyMap . IntMap.toList
  
  instance (Pretty k, Pretty v) => Pretty (Map k v) where
    pretty = prettyMap . Map.toList
  
  -- Pretty instances for dependencies of this module (to avoid dependency cycles)
  
  instance Pretty AbsolutePath where
    pretty = text . filePath
  
  instance Pretty RangeFile where
    pretty = pretty . rangeFilePath
  
  prettyLineColumn :: Position' a -> Doc
  prettyLineColumn (Pn _ _ l c) = pretty l <> dot <> pretty c
  
  instance Pretty a => Pretty (Position' (Strict.Maybe a)) where
    pretty p = case srcFile p of
      Strict.Nothing -> prettyLineColumn p
      Strict.Just f  -> pretty f <> colon <> prettyLineColumn p
  
  instance Pretty PositionWithoutFile where
    pretty = prettyLineColumn
  
  instance Pretty IntervalWithoutFile where
    pretty (Interval () s e)
      | s == e    = start
      | otherwise = start <> "-" <> end
      where
        sl = posLine s
        el = posLine e
        sc = posCol s
        ec = posCol e
  
        start :: Doc
        start = pretty sl <> dot <> pretty sc
  
        end :: Doc
          | sl == el  = pretty ec
          | otherwise = pretty el <> dot <> pretty ec
  
  instance Pretty a => Pretty (Interval' (Strict.Maybe a)) where
    pretty i@(Interval f s e) = file <> pretty (Interval () s e)
      where
        file :: Doc
        file = case f of
                 Strict.Nothing -> empty
                 Strict.Just f  -> pretty f <> colon
  
  instance Pretty a => Pretty (Range' (Strict.Maybe a)) where
    pretty r = maybe empty pretty (rangeToIntervalWithFile r)
  
  instance (Pretty a, HasRange a) => Pretty (PrintRange a) where
    pretty (PrintRange a) = pretty a <+> parens ("at" <+> pretty (getRange a))
  
  
  ---------------------------------------------------------------------------
  -- * Generalizing the original type from list to Foldable
  
  sep, fsep, hsep, hcat, vcat :: Foldable t => t Doc -> Doc
  sep  = P.sep  . Fold.toList
  fsep = P.fsep . Fold.toList
  hsep = P.hsep . Fold.toList
  hcat = P.hcat . Fold.toList
  vcat = P.vcat . Fold.toList
  
  punctuate :: Foldable t => Doc -> t Doc -> [Doc]
  punctuate d = P.punctuate d . Fold.toList
  
  ---------------------------------------------------------------------------
  -- * 'Doc' utilities
  
  vsep :: [Doc] -> Doc
  vsep = vcat . List.intersperse ""
  
  pwords :: String -> [Doc]
  pwords = map text . words
  
  fwords :: String -> Doc
  fwords = fsep . pwords
  
  -- | Separate, but only if both separees are not null.
  
  hsepWith :: Doc -> Doc -> Doc -> Doc
  hsepWith sep d1 d2
    | null d2   = d1
    | null d1   = d2
    | otherwise = d1 <+> sep <+> d2
  
  -- | Comma separated list, without the brackets.
  prettyList_ :: Pretty a => [a] -> Doc
  prettyList_ = fsep . punctuate comma . map pretty
  
  -- | Pretty print a set.
  prettySet :: Pretty a => [a] -> Doc
  prettySet = braces . prettyList_
  
  -- | Pretty print an association list.
  prettyMap :: (Pretty k, Pretty v) => [(k,v)] -> Doc
  prettyMap = braces . fsep . punctuate comma . map prettyAssign
  
  -- | Pretty print a single association.
  prettyAssign :: (Pretty k, Pretty v) => (k,v) -> Doc
  prettyAssign (k, v) = sep [ prettyPrec 1 k <+> hlSymbol "->", nest 2 $ pretty 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 True  = parens
  mparens False = id
  
  -- | Only wrap in parens if not 'empty'
  parensNonEmpty :: Doc -> Doc
  parensNonEmpty d = if null d then empty else parens d
  
  -- | Return 'empty' for empty strings.
  textNonEmpty :: String -> Doc
  textNonEmpty = \case
    "" -> empty
    s  -> text s
  
  -- | @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
  
  infixl 6 <?>
  -- | @a <?> b = hang a 2 b@
  (<?>) :: Doc -> Doc -> Doc
  a <?> b = hang a 2 b
  
  -- | @pshow = text . show@
  pshow :: Show a => a -> Doc
  pshow = text . show
  
  singPlural :: Sized a => a -> c -> c -> c
  singPlural xs singular plural = if natSize xs == 1 then singular else plural
  
  pluralS :: Sized a => a -> Doc -> Doc
  pluralS xs d = singPlural xs d (d <> "s")
  
  -- | Used for with-like 'telescopes'
  
  prefixedThings :: Doc -> [Doc] -> Doc
  prefixedThings kw = \case
    []           -> P.empty
    (doc : docs) -> fsep $ (kw <+> doc) : map (hlSymbol "|" <+>) docs
  
  ---------------------------------------------------------------------------
  -- * Annotations
  
  -- | Only adds an annotation node if the 'Aspects' is non-'null'.
  annotate :: Aspects -> Doc -> Doc
  annotate a x
    | null a    = x
    | otherwise = rnf a `seq` P.annotate a x
  
  -- | Attach a simple 'Aspect', rather than a full set of 'Aspects', to a
  -- document.
  annotateAspect :: Aspect -> Doc -> Doc
  annotateAspect a = annotate a' where
    a' = Aspects
      { aspect         = Just a
      , otherAspects   = mempty
      , note           = ""
      , definitionSite = Nothing
      , tokenBased     = TokenBased
      }
  
  -- * Hyperlink annotations
  
  -- | Attach a link to a document (cf. LaTeX @\href@).
  href :: Text -> Doc -> Doc
  href = annotateAspect . URL
  
  -- | A URL formatted as link (cf. LaTeX @\url@).
  url :: String -> Doc
  url s = href (Text.pack s) (text s)
  
  -- | Link to an issue on the Agda bug tracker.
  githubIssue :: Int -> Doc
  githubIssue = url . ("https://github.com/agda/agda/issues/" ++) . show
  
  -- | Attach the position of something as the "binding site" of a 'Doc'.
  definedAt :: HasRange a => Doc -> a -> Doc
  definedAt doc p = annotate (rangeDefinitionSite p) doc
  
  -- ** Basic syntax highlighting helpers
  
  hlComment, hlSymbol, hlKeyword, hlString, hlNumber, hlHole, hlPrimitiveType, hlPragma
    :: Doc -> Doc
  
  hlComment       = annotateAspect Comment
  hlSymbol        = annotateAspect Symbol
  hlKeyword       = annotateAspect Keyword
  hlString        = annotateAspect String
  hlNumber        = annotateAspect Number
  hlHole          = annotateAspect Hole
  hlPrimitiveType = annotateAspect PrimitiveType
  hlPragma        = annotateAspect Pragma
  
  -- ** Helpers introducing 'NameKind's
  
  hlNameKind :: NameKind -> Doc -> Doc
  hlNameKind k = annotateAspect (Name (Just k) False)
  
  hlBound, hlGeneralizable, hlDatatype, hlField,
    hlFunction, hlModule, hlPostulate, hlPrimitive, hlRecord, hlArgument,
    hlMacro :: Doc -> Doc
  
  hlBound         = hlNameKind Bound
  hlGeneralizable = hlNameKind Generalizable
  hlDatatype      = hlNameKind Datatype
  hlField         = hlNameKind Field
  hlFunction      = hlNameKind Function
  hlModule        = hlNameKind Module
  hlPostulate     = hlNameKind Postulate
  hlPrimitive     = hlNameKind Primitive
  hlRecord        = hlNameKind Record
  hlArgument      = hlNameKind Argument
  hlMacro         = hlNameKind Macro
  
  hlConstructor :: Induction -> Doc -> Doc
  hlConstructor = hlNameKind . Constructor
  
  ---------------------------------------------------------------------------
  -- * Delimiter wrappers
  --
  -- These use the 'Symbol' highlight for the punctuation characters.
  
  parens       :: Doc -> Doc -- ^ Wrap document in @(...)@
  brackets     :: Doc -> Doc -- ^ Wrap document in @[...]@
  braces       :: Doc -> Doc -- ^ Wrap document in @{...}@
  quotes       :: Doc -> Doc -- ^ Wrap document in @\'...\'@
  doubleQuotes :: Doc -> Doc -- ^ Wrap document in @\"...\"@
  quotes p       = hlSymbol (char '\'') <> p <> hlSymbol (char '\'')
  doubleQuotes p = hlSymbol (char '"') <> p <> hlSymbol (char '"')
  parens p       = lparen <> p <> rparen
  brackets p     = lbrack <> p <> rbrack
  braces p       = lbrace <> p <> rbrace
  
  semi, comma, colon, dot, pipe, equals, lparen, rparen, lbrack, rbrack, lbrace, rbrace :: Doc
  semi   = hlSymbol $ char ';'
  comma  = hlSymbol $ char ','
  colon  = hlSymbol $ char ':'
  dot    = hlSymbol $ char '.'
  pipe   = hlSymbol $ char '|'
  equals = hlSymbol $ char '='
  lparen = hlSymbol $ char '('
  rparen = hlSymbol $ char ')'
  lbrack = hlSymbol $ char '['
  rbrack = hlSymbol $ char ']'
  lbrace = hlSymbol $ char '{'
  rbrace = hlSymbol $ char '}'
  