module Agda.Utils.CallStack.Pretty
  ( -- This module only exports instances.
  ) where

import Agda.Utils.CallStack.Base
  ( CallSite
  , CallStack
  , SrcLoc(..)
  , getCallStack
  )
import Agda.Utils.Pretty
  ( (<+>), ($+$), (<>)
  , pshow, text
  , colon, comma
  , nest, parens
  , hcat, hsep, vcat
  , Pretty(pretty)
  )

instance Pretty SrcLoc where
  pretty :: SrcLoc -> Doc
pretty SrcLoc {Int
[Char]
srcLocPackage :: SrcLoc -> [Char]
srcLocModule :: SrcLoc -> [Char]
srcLocFile :: SrcLoc -> [Char]
srcLocStartLine :: SrcLoc -> Int
srcLocStartCol :: SrcLoc -> Int
srcLocEndLine :: SrcLoc -> Int
srcLocEndCol :: SrcLoc -> Int
srcLocEndCol :: Int
srcLocEndLine :: Int
srcLocStartCol :: Int
srcLocStartLine :: Int
srcLocFile :: [Char]
srcLocModule :: [Char]
srcLocPackage :: [Char]
..} = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [Doc
physicalLoc, Doc
"in", Doc
logicalLoc]
      where
        physicalLoc :: Doc
physicalLoc = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [[Char] -> Doc
text [Char]
srcLocFile, Doc
colon, Int -> Doc
forall a. Show a => a -> Doc
pshow Int
srcLocStartLine, Doc
colon, Int -> Doc
forall a. Show a => a -> Doc
pshow Int
srcLocStartCol]
        logicalLoc :: Doc
logicalLoc = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [[Char] -> Doc
text [Char]
srcLocPackage, Doc
colon, [Char] -> Doc
text [Char]
srcLocModule]

instance Pretty CallSite where
  pretty :: CallSite -> Doc
pretty ([Char]
fun, SrcLoc
loc) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [[Char] -> Doc
text [Char]
fun Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma, Doc
"called at", SrcLoc -> Doc
forall a. Pretty a => a -> Doc
pretty SrcLoc
loc]

instance Pretty CallStack where
  pretty :: CallStack -> Doc
pretty CallStack
cs = case (CallSite -> Doc) -> [CallSite] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CallSite -> Doc
forall a. Pretty a => a -> Doc
pretty (CallStack -> [CallSite]
getCallStack CallStack
cs) of
    []                  -> Doc -> Doc
parens Doc
"empty CallStack"
    Doc
firstLoc : [Doc]
restLocs -> Doc
firstLoc Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [Doc]
restLocs)